Termination Proof Script
Consider the TRS R consisting of the rewrite rules
|
| 1: |
|
active(g(X)) |
→ mark(h(X)) |
| 2: |
|
active(c) |
→ mark(d) |
| 3: |
|
active(h(d)) |
→ mark(g(c)) |
| 4: |
|
proper(g(X)) |
→ g(proper(X)) |
| 5: |
|
proper(h(X)) |
→ h(proper(X)) |
| 6: |
|
proper(c) |
→ ok(c) |
| 7: |
|
proper(d) |
→ ok(d) |
| 8: |
|
g(ok(X)) |
→ ok(g(X)) |
| 9: |
|
h(ok(X)) |
→ ok(h(X)) |
| 10: |
|
top(mark(X)) |
→ top(proper(X)) |
| 11: |
|
top(ok(X)) |
→ top(active(X)) |
|
There are 12 dependency pairs:
|
| 12: |
|
ACTIVE(g(X)) |
→ H(X) |
| 13: |
|
ACTIVE(h(d)) |
→ G(c) |
| 14: |
|
PROPER(g(X)) |
→ G(proper(X)) |
| 15: |
|
PROPER(g(X)) |
→ PROPER(X) |
| 16: |
|
PROPER(h(X)) |
→ H(proper(X)) |
| 17: |
|
PROPER(h(X)) |
→ PROPER(X) |
| 18: |
|
G(ok(X)) |
→ G(X) |
| 19: |
|
H(ok(X)) |
→ H(X) |
| 20: |
|
TOP(mark(X)) |
→ TOP(proper(X)) |
| 21: |
|
TOP(mark(X)) |
→ PROPER(X) |
| 22: |
|
TOP(ok(X)) |
→ TOP(active(X)) |
| 23: |
|
TOP(ok(X)) |
→ ACTIVE(X) |
|
The approximated dependency graph contains 4 SCCs:
{18},
{19},
{15,17}
and {20,22}.
-
Consider the SCC {18}.
There are no usable rules.
By taking the AF π with
π(G) = 1 together with
the lexicographic path order with
empty precedence,
rule 18
is strictly decreasing.
-
Consider the SCC {19}.
There are no usable rules.
By taking the AF π with
π(H) = 1 together with
the lexicographic path order with
empty precedence,
rule 19
is strictly decreasing.
-
Consider the SCC {15,17}.
There are no usable rules.
By taking the AF π with
π(g) = π(PROPER) = 1 together with
the lexicographic path order with
empty precedence,
rule 15
is weakly decreasing and
rule 17
is strictly decreasing.
There is one new SCC.
-
Consider the SCC {15}.
By taking the AF π with
π(PROPER) = 1 together with
the lexicographic path order with
empty precedence,
rule 15
is strictly decreasing.
-
Consider the SCC {20,22}.
The usable rules are {1-9}.
The constraints could not be solved.
Tyrolean Termination Tool (6.59 seconds)
--- May 4, 2006